Inference at * 2 1 
Iof proof for Lemma before-adjacent:



1. T : Type
2. T List
3. u : T
4. v : T List
5. x, y:T.
5. no_repeats(T;v)  adjacent(T;v;x;y)  (z:T. z before y  v  (z before x  v  (z = x)))
6. x : T
7. y : T
8. no_repeats(T;[u / v])
9. 0 < ||v||
10. x = u & y = hd(v)
11. z : T
12. z before y  [u / v]
  z before x  [u / v]  (z = x) 

latex

 by InteriorProof ((RWO "cons_before" (0)) 
CollapseTHENA (Auto)) 

latex

C1: 

C1:   ((z = u & (x  v))  z before x  v)  (z = x)
C.

Definitions	P  Q, P  Q, P  Q, [car / cdr], P  Q, left + right, (x  l), , t  T, P & Q, x:A  B(x), hd(l), x before y  l, a < b, no_repeats(T;l), x:A. B(x), x:AB(x), type List, Type, s = t
Lemmas	or functionality wrt iff, cons before, iff wf, rev implies wf, l member wf, l before wf